<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>Tokenizer</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="Tokenizer";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/mmio/Systemizer.html" title="class in mmj.mmio"><span class="strong">Prev Class</span></a></li>
<li>Next Class</li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/mmio/Tokenizer.html" target="_top">Frames</a></li>
<li><a href="Tokenizer.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.mmio</div>
<h2 title="Class Tokenizer" class="title">Class Tokenizer</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.mmio.Tokenizer</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">Tokenizer</span>
extends java.lang.Object</pre>
<div class="block">Parse a Metamath .mm file into Metamath tokens.
 <p>
 This class (presently) provides input services for a MetaMath.mm file. Its
 primary purpose is to return MetaMath tokens, but if desired, the whitespace
 in between tokens can be obtained, as well as other information.
 <p>
 Note: this file validates the input file to ensure that only valid characters
 are present. These are the various 7-bit ASCII printable characters and white
 space characters documented in metamath.pdf at www.metamath.org. ANSI or DOS
 (cr or cr/lf) line terminators are accepted and are considered part of the
 white space. Invalid characters will generate a MMIOError exception (a FAR
 more serious problem than a mere MetaMathParseException exception ;-)
 <p>
 Note: Tokenizer should work with UTF-8 and other character sets that code the
 7-bit ASCII characters the same way(?), but because it uses hard coded values
 it would need to be cloned if someone wants to be able to input full Unicode
 (an interface could be developed.)
 <p>
 Note: This class does not expand MetaMath include statements (i.e.
 "$[ infiniteset.mm $]"). That feat can be handled in the parsing logic --
 this is just a simple, uneducated tokenizer class. Or....conveniently use the
 technique described in mmverify.py at www.metamath.org.
 <p>
 (from mmverify.py): "Before using this program, any compressed proofs must be
 expanded with the Metamath program, e.g.:
 <p>
 <code>$ ./metamath 'r set.mm' 'sa p *' 'w s set.mm' q &gt; /dev/null</code>
 <p>
 That somewhat cryptic (unix/linux) command says 1) Read file set.mm; 2) Save
 all proofs in default format (uncompressed); 3) Save to disk; and 4) (?) send
 Metamath output commentary about what it is being asked to do to to the bit
 bucket...
 <p>
 Here's a version from a Windows ".bat" file that saves the expanded file to a
 different file name:
 <p>
 <code>metamath.exe "r myset.mm" "v proof *" "sa p *" "w s expmyset.mm" "exit" &gt;&gt; expmyset.txt</code></div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/mmio/Tokenizer.html#Tokenizer(java.io.Reader, java.lang.String)">Tokenizer</a></strong>(java.io.Reader&nbsp;r,
         java.lang.String&nbsp;s)</code>
<div class="block">Constructs Tokenizer from a Reader.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/mmio/Tokenizer.html#Tokenizer(java.io.Reader, java.lang.String, long)">Tokenizer</a></strong>(java.io.Reader&nbsp;r,
         java.lang.String&nbsp;s,
         long&nbsp;nbrCharsToBypass)</code>
<div class="block">Constructs Tokenizer from a Reader, with "skipahead n", where n =
 nbrCharsToBypass.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#close()">close</a></strong>()</code>
<div class="block">Close file/reader.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>long</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#countNbrLines()">countNbrLines</a></strong>()</code>
<div class="block">Count number of lines in input file.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>long</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#getCurrentCharNbr()">getCurrentCharNbr</a></strong>()</code>
<div class="block">Return current character number in the file.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>long</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#getCurrentColumnNbr()">getCurrentColumnNbr</a></strong>()</code>
<div class="block">Return current column number in the current line in the file.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>long</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#getCurrentLineNbr()">getCurrentLineNbr</a></strong>()</code>
<div class="block">Return current line number in the file.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#getSourceId()">getSourceId</a></strong>()</code>
<div class="block">Get "Source Id" for the file (for use in error/diagnostic/testing
 messages.)</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#getToken(java.lang.StringBuilder, int)">getToken</a></strong>(java.lang.StringBuilder&nbsp;strBuf,
        int&nbsp;offset)</code>
<div class="block">
 Gets next MetaMath token from the input file and stores it in
 <code>strBuf</code>.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/mmio/Tokenizer.html#getWhiteSpace(java.lang.StringBuilder, int)">getWhiteSpace</a></strong>(java.lang.StringBuilder&nbsp;strBuf,
             int&nbsp;offset)</code>
<div class="block">Gets next chunk of whitespace from MetaMath file and stores it in
 <code>strBuf</code>.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="Tokenizer(java.io.Reader, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Tokenizer</h4>
<pre>public&nbsp;Tokenizer(java.io.Reader&nbsp;r,
         java.lang.String&nbsp;s)
          throws java.io.IOException</pre>
<div class="block">Constructs Tokenizer from a Reader.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>r</code> - Reader (may be StringReader or BufferedReader but PushbackReader
            and LineNumberReader are not helpful choices.)</dd><dd><code>s</code> - Source Id Text, such as filename or test ID. May be empty string
            if N/A. Used solely for diagnostic messages.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if I/O error</dd></dl>
</li>
</ul>
<a name="Tokenizer(java.io.Reader, java.lang.String, long)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>Tokenizer</h4>
<pre>public&nbsp;Tokenizer(java.io.Reader&nbsp;r,
         java.lang.String&nbsp;s,
         long&nbsp;nbrCharsToBypass)
          throws java.io.IOException,
                 java.lang.IllegalArgumentException</pre>
<div class="block">Constructs Tokenizer from a Reader, with "skipahead n", where n =
 nbrCharsToBypass.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>r</code> - Reader (may be StringReader or BufferedReader but PushbackReader
            and LineNumberReader are not helpful choices.)</dd><dd><code>s</code> - Source Id Text, such as filename or test ID. May be empty string
            if N/A. Used solely for diagnostic messages.</dd><dd><code>nbrCharsToBypass</code> - Used to reposition reader with previously
            returned charNbr from <code>getCurrentCharNbr</code> method.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if I/O error</dd>
<dd><code>java.lang.IllegalArgumentException</code> - if <code>nbrCharsToBypass
        is less than zero.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="getToken(java.lang.StringBuilder, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getToken</h4>
<pre>public&nbsp;int&nbsp;getToken(java.lang.StringBuilder&nbsp;strBuf,
           int&nbsp;offset)
             throws java.io.IOException</pre>
<div class="block"><p>
 Gets next MetaMath token from the input file and stores it in
 <code>strBuf</code>.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>strBuf</code> - the <code>StringBuilder</code> where the next available MetaMath
            token will be inserted</dd><dd><code>offset</code> - insertion point offset in strBuf for token. (If strBuf
            contains 3 characters then set offset to 3 because it is
            relative to zero.)</dd>
<dt><span class="strong">Returns:</span></dt><dd>length of token, or -1 if EOF reached.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if I/O error</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if invalid character read</dd></dl>
</li>
</ul>
<a name="getWhiteSpace(java.lang.StringBuilder, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getWhiteSpace</h4>
<pre>public&nbsp;int&nbsp;getWhiteSpace(java.lang.StringBuilder&nbsp;strBuf,
                int&nbsp;offset)
                  throws java.io.IOException</pre>
<div class="block">Gets next chunk of whitespace from MetaMath file and stores it in
 <code>strBuf</code>.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>strBuf</code> - the <code>StringBuilder</code> where the next whitespace chunk
            will be inserted</dd><dd><code>offset</code> - insertion point offset in strBuf for whitespace</dd>
<dt><span class="strong">Returns:</span></dt><dd>length of whitespace, zero if next char on file is start of
         token, or -1 if EOF reached.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if I/O error</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if invalid character read</dd></dl>
</li>
</ul>
<a name="getCurrentLineNbr()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCurrentLineNbr</h4>
<pre>public&nbsp;long&nbsp;getCurrentLineNbr()</pre>
<div class="block">Return current line number in the file.
 <p>
 Current line number corresponds to the line number of the last token or
 whitespace chunk returned.
 <p>
 Line number is incremented when a character is processed AFTER end of
 line.
 <p>
 Note: "cr/lf" and "cr" are valid line terminators. Using them in
 combination is inadvisable. The algorithm used here differs from the Java
 language algorithm in that cr/cr/lf is counted as TWO line terminators
 instead of just one (and cr/cr/cr/lf is 3, etc.)</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>current line number in the file (starts with 1).</dd></dl>
</li>
</ul>
<a name="getCurrentColumnNbr()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCurrentColumnNbr</h4>
<pre>public&nbsp;long&nbsp;getCurrentColumnNbr()</pre>
<div class="block">Return current column number in the current line in the file.
 <p>
 Note: tab characters are ignored for purposes of computing column number.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>current column number (starts with 1).</dd></dl>
</li>
</ul>
<a name="getCurrentCharNbr()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCurrentCharNbr</h4>
<pre>public&nbsp;long&nbsp;getCurrentCharNbr()</pre>
<div class="block">Return current character number in the file.
 <p>
 Following getToken or getWhiteSpace this will be the character number of
 the last character returned in the token or whitespace.
 <p>
 Intended to be used with startPosition method, say, with MetaMath file
 include processing which closes a reader and then re-starts where it left
 off.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>current column number (starts with 1).</dd></dl>
</li>
</ul>
<a name="getSourceId()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSourceId</h4>
<pre>public&nbsp;java.lang.String&nbsp;getSourceId()</pre>
<div class="block">Get "Source Id" for the file (for use in error/diagnostic/testing
 messages.)</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>sourceId</dd></dl>
</li>
</ul>
<a name="close()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>close</h4>
<pre>public&nbsp;void&nbsp;close()</pre>
<div class="block">Close file/reader.</div>
</li>
</ul>
<a name="countNbrLines()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>countNbrLines</h4>
<pre>public&nbsp;long&nbsp;countNbrLines()
                   throws java.io.IOException</pre>
<div class="block">Count number of lines in input file.
 <p>
 This is provided for testing purposes. Delete if desired. Since rewind()
 is not supported, use of countNbrLines cannot be mixed with other
 functions -- it is a one-shot use of a newly constructed Tokenizer, and a
 new Tokenizer would need to be constructed for other uses.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>number of lines in the file.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if I/O error</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/mmio/Systemizer.html" title="class in mmj.mmio"><span class="strong">Prev Class</span></a></li>
<li>Next Class</li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/mmio/Tokenizer.html" target="_top">Frames</a></li>
<li><a href="Tokenizer.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
